;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "iimage.lisp")
(require "icommon.lisp")

(module MImage
  (import ICommon)
  
  (include-book "avl-rational-keys" :dir :teachpacks)
  
  
  (defun cut (list i)
     (if (equal i 0)
         list
         (cut (cdr list) (- i 1))))
  
  (defun insertInt (list index object i)
    (if (equal i index)
        (append object (cut list (len object)))
        (cons (car list) (insertInt (cdr list) index object (+ i 1)))))
  
   (defun insertAt (list index object)
    (insertInt list index object 1))
  
  (defun createRGB(r g b)
    (list r g b))
  
  (defun insertPixel(tree x y r g b)
    (let* ((rgb (createRGB r g b)))
      (if (occurs-in-tree? y tree)
          (avl-insert tree y (avl-insert (cdr (avl-retrieve tree y)) x rgb))
          (avl-insert tree y (avl-insert (empty-tree) x rgb)))))
  
  (defun getPixel(tree x y)
    (cdr (avl-retrieve (cdr (avl-retrieve tree y)) x)))
  
  (defun getNextXCoordinate (x width)
    (if (> (+ x 1) width)
        1
        (+ x 1)))
  
  (defun getNextYCoordinate (x y width)
    (if (> (+ x 1) width)
        (- y 1)
        y))
        
  (defun isValidPixel(x y width height)
    (and (>= x 1) (<= x width) (>= y 1) (<= y height)))
  
  (defun readPixels(tree pixels width height count)
    (let* ((b (car   pixels))
           (g (cadr  pixels))
           (r (caddr pixels)) 
           (x (+ (mod (- count 1) width) 1))
           (y (- height (floor (- count 1) width))))
      (if (consp pixels)
          (if (equal (mod count width) 0)
              (readPixels (insertPixel tree x y r g b) (remainingElements pixels (+ 3 (mod width 4))) width height (+ count 1) );;Padding for 4byte alignment
              (readPixels (insertPixel tree x y r g b) (remainingElements pixels 3) width height (+ count 1) ))
          tree)))
  
  (defun GenerateBitmapPadding (x)
    (if (> x 0)
        (cons 0 (GenerateBitmapPadding (- x 1)))
        nil))
  
  (defun writePixels(tree x y width height count)
    (if (<= y 0)
        nil
        (let* ((rgb (getPixel tree x y)))
          (let* ((nextX (if (equal x width)
                            1
                            (+ x 1)))
                 (nextY (if (equal x width)
                            (- y 1)
                            y)))
            (if (equal (mod count width) 0)
                (append (append (list (caddr rgb)) (list (cadr rgb)) (list (car rgb)) (GenerateBitmapPadding (mod width 4))) (writePixels tree nextX nextY width height (+ count 1)))
                (append (list  (caddr rgb) (cadr rgb) (car rgb)    ) (writePixels tree nextX nextY width height (+ count 1))))))))
  
  (defun getHeader(tree)
    (cdr (avl-retrieve tree -1)))
  
  (defun getWidth(tree)
    (cdr (avl-retrieve tree -2)))
  
  (defun getHeight(tree)
    (cdr (avl-retrieve tree -3)))
  
  (defun setWidth(tree width)
    (avl-insert tree -2 width))
  
  (defun setHeight(tree height)
    (avl-insert tree -3 height))
  
  
    
    
  
  (defun bmp->tree (bmpBytes)
    (let* ((BChar        (getElement bmpBytes 1))
           (MChar        (getElement bmpBytes 2))
           (Size1        (getElement bmpBytes 3)) ; bytes in entire file
           (Size2        (getElement bmpBytes 4))
           (Size3        (getElement bmpBytes 5))
           (Size4        (getElement bmpBytes 6))
           (App1         (getElement bmpBytes 7))
           (App2         (getElement bmpBytes 8))
           (App3         (getElement bmpBytes 9))
           (App4         (getElement bmpBytes 10))
           (Offset1      (getElement bmpBytes 11))
           (Offset2      (getElement bmpBytes 12))
           (Offset3      (getElement bmpBytes 13))
           (Offset4      (getElement bmpBytes 14))
           (DIBSize1     (getElement bmpBytes 15))
           (DIBSize2     (getElement bmpBytes 16))
           (DIBSize3     (getElement bmpBytes 17))
           (DIBSize4     (getElement bmpBytes 18))
           (Width1       (getElement bmpBytes 19))
           (Width2       (getElement bmpBytes 20))
           (Width3       (getElement bmpBytes 21))
           (Width4       (getElement bmpBytes 22))
           (Height1      (getElement bmpBytes 23))
           (Height2      (getElement bmpBytes 24))
           (Height3      (getElement bmpBytes 25))
           (Height4      (getElement bmpBytes 26))
           (Plane1       (getElement bmpBytes 27))
           (Plane2       (getElement bmpBytes 28))
           (BitsPerPixel1(getElement bmpBytes 29))
           (BitsPerPixel2(getElement bmpBytes 30))
           (BIRGB1       (getElement bmpBytes 31))
           (BIRGB2       (getElement bmpBytes 32))
           (BIRGB3       (getElement bmpBytes 33))
           (BIRGB4       (getElement bmpBytes 34))
           (Size1        (getElement bmpBytes 35)) ; bytes in array, inc padding
           (Size2        (getElement bmpBytes 36))
           (Size3        (getElement bmpBytes 37))
           (Size4        (getElement bmpBytes 38))
           (HorizRes1    (getElement bmpBytes 39))
           (HorizRes2    (getElement bmpBytes 40))
           (HorizRes3    (getElement bmpBytes 41))
           (HorizRes4    (getElement bmpBytes 42))
           (VertRes1     (getElement bmpBytes 43))
           (VertRes2     (getElement bmpBytes 44))
           (VertRes3     (getElement bmpBytes 45))
           (VertRes4     (getElement bmpBytes 46))
           (NumColors1   (getElement bmpBytes 47))
           (NumColors2   (getElement bmpBytes 48))
           (NumColors3   (getElement bmpBytes 49))
           (NumColors4   (getElement bmpBytes 50))
           (ImpColors1   (getElement bmpBytes 51))
           (ImpColors2   (getElement bmpBytes 52))
           (ImpColors3   (getElement bmpBytes 53))
           (ImpColors4   (getElement bmpBytes 54))
           (Header       (getElements bmpBytes 1 54))
           (Pixels       (remainingElements bmpBytes 54))
           (Width        (HexCalculate (list Width1 Width2 Width3 Width4)))
           (Height       (HexCalculate (list Height1 Height2 Height3 Height4)))
           (BitDepth     (HexCalculate (list BitsPerPixel1 BitsPerPixel2))))
      (if (not (equal BitDepth 24))
          (mv nil (list "Image is not a 24 bit image"))
          (mv (readPixels (avl-insert (avl-insert (avl-insert (empty-tree) -1 Header) -2 Width) -3 Height) Pixels Width Height 1) nil))))

  (defun updatedHeader (tree)
    (let* ((Header        (getHeader tree))
           (Width         (getWidth tree))
           (Height        (getHeight tree))
           (sizewheader   (GetBMPSize width height))
           (size          (- sizewheader 54)))
      (insertAt ;insert height
       (insertAt ;insert the width
        (insertAt ; insert size of just the pixel array
         (insertAt Header 3 (int->bytes sizewheader)) ; insert size of the entire image
         35 (int->bytes size))
        19 (int->bytes width))
       23 (int->bytes height))
      ))
  
;Old Update Header (for comparison)
;  (defun updatedHeader (tree)
;    (let* ((Header (getHeader tree))
;           (Width  (getWidth tree))
;           (Height (getHeight tree))
;           (paddedwidth (* (ceiling (* Height 3) 4) 4))
;           (size   (* Height paddedwidth))
;           (sizewheader (+ size 54)))
;      (insertAt ;insert height
;      (insertAt ;insert the width
;      (insertAt ; insert size of just the pixel array
;       (insertAt Header 3 (int->bytes sizewheader)) ; insert size of the entire image
;        35 (int->bytes size))
;      19 (int->bytes width))
;      23 (int->bytes height))
;      ))
    
  
   (defun tree->bmp(tree)
    (let* ((Header        (updatedHeader tree));Get UpdateHeader working and replace.
           (Width         (getWidth  tree))
           (Height        (getHeight tree)))
      (append Header (writePixels tree 1 Height  Width Height 1))))
 
  
  (export IImage))